A:es_realizer{i:l}. R-compat{i:l}(Rnone; A) 

latex

Definitions	ge(i; j), False, A, A  B, tt, ff, True, Rnone?(x1), Rplus-right(x1), Rplus-left(x1), P  Q, Rplus?(x1), if b then t else f fi , Y, prop{i:l}, t  T, P  Q, R-compat{i:l}(A; B), x:A. B(x), , guard(T), P  Q, Unit, , , , subtype(S; T)
Lemmas	ge wf, nat properties, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Rplus-right wf, Rplus-left wf, R-size-decreases, eqtt to assert, bool wf, Rplus? wf, le wf, es realizer wf, nat plus wf, nat plus inc, R-size wf, nat wf